Inference at * 1 
Iof proof for Lemma p-fun-exp-add1-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. n : 
5. isl(f(x))
  (f^n+1(x)) ~ (f^n(outl(f(x)))) 

latex

 by (Unfold `p-fun-exp` ( 0)) 
CollapseTHEN (((RWO "simple-primrec-add" 0) 
CollapseTHENA (Auto
C)) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN ((NatInd (-2)) 
CollapseTHEN (Reduce 0))))
C 

latex

C1: 

C1: 4. isl(f(x))
C1:   (f o p-id()  (x)) ~ (p-id()(outl(f(x))))
C2: .....upcase..... NILNIL

C2: 4. isl(f(x))
C2: 5. n : 
C2: 6. 0 < n
C2: 7. (primrec(n - 1;f o p-id()  ;i,g. f o g  )(x))
C2: 7. ~
C2: 7. (primrec(n - 1;p-id();i,g. f o g  )(outl(f(x))))
C2:   (primrec(n;f o p-id()  ;i,g. f o g  )(x)) ~ (primrec(n;p-id();i,g. f o g  )(outl(f(x))))
C.

Definitions	n - m, n+m, -n, s ~ t, i  j , f^n, Top, x:A.B(x), , , {x:A| B(x)} , A, False, P  Q, x:AB(x), Void, a < b, #$n, A  B, x:A. B(x), t  T
Lemmas	ge wf, nat properties, simple-primrec-add, le wf